(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
U11(tt, N, XS) → U12(tt, activate(N), activate(XS))
U12(tt, N, XS) → snd(splitAt(activate(N), activate(XS)))
U21(tt, X) → U22(tt, activate(X))
U22(tt, X) → activate(X)
U31(tt, N) → U32(tt, activate(N))
U32(tt, N) → activate(N)
U41(tt, N, XS) → U42(tt, activate(N), activate(XS))
U42(tt, N, XS) → head(afterNth(activate(N), activate(XS)))
U51(tt, Y) → U52(tt, activate(Y))
U52(tt, Y) → activate(Y)
U61(tt, N, X, XS) → U62(tt, activate(N), activate(X), activate(XS))
U62(tt, N, X, XS) → U63(tt, activate(N), activate(X), activate(XS))
U63(tt, N, X, XS) → U64(splitAt(activate(N), activate(XS)), activate(X))
U64(pair(YS, ZS), X) → pair(cons(activate(X), YS), ZS)
U71(tt, XS) → U72(tt, activate(XS))
U72(tt, XS) → activate(XS)
U81(tt, N, XS) → U82(tt, activate(N), activate(XS))
U82(tt, N, XS) → fst(splitAt(activate(N), activate(XS)))
afterNth(N, XS) → U11(tt, N, XS)
fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)
natsFrom(N) → cons(N, n__natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)
snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → U61(tt, N, X, activate(XS))
tail(cons(N, XS)) → U71(tt, activate(XS))
take(N, XS) → U81(tt, N, XS)
natsFrom(X) → n__natsFrom(X)
activate(n__natsFrom(X)) → natsFrom(X)
activate(X) → X
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1))
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1)))
U21(tt, z0) → U22(tt, activate(z0))
U22(tt, z0) → activate(z0)
U31(tt, z0) → U32(tt, activate(z0))
U32(tt, z0) → activate(z0)
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1))
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1)))
U51(tt, z0) → U52(tt, activate(z0))
U52(tt, z0) → activate(z0)
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2))
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2))
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1))
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1)
U71(tt, z0) → U72(tt, activate(z0))
U72(tt, z0) → activate(z0)
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1))
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1)))
afterNth(z0, z1) → U11(tt, z0, z1)
fst(pair(z0, z1)) → U21(tt, z0)
head(cons(z0, z1)) → U31(tt, z0)
natsFrom(z0) → cons(z0, n__natsFrom(s(z0)))
natsFrom(z0) → n__natsFrom(z0)
sel(z0, z1) → U41(tt, z0, z1)
snd(pair(z0, z1)) → U51(tt, z1)
splitAt(0, z0) → pair(nil, z0)
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2))
tail(cons(z0, z1)) → U71(tt, activate(z1))
take(z0, z1) → U81(tt, z0, z1)
activate(n__natsFrom(z0)) → natsFrom(z0)
activate(z0) → z0
Tuples:
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U21'(tt, z0) → c2(U22'(tt, activate(z0)), ACTIVATE(z0))
U22'(tt, z0) → c3(ACTIVATE(z0))
U31'(tt, z0) → c4(U32'(tt, activate(z0)), ACTIVATE(z0))
U32'(tt, z0) → c5(ACTIVATE(z0))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U51'(tt, z0) → c8(U52'(tt, activate(z0)), ACTIVATE(z0))
U52'(tt, z0) → c9(ACTIVATE(z0))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1))
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2))
U71'(tt, z0) → c14(U72'(tt, activate(z0)), ACTIVATE(z0))
U72'(tt, z0) → c15(ACTIVATE(z0))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
FST(pair(z0, z1)) → c19(U21'(tt, z0))
HEAD(cons(z0, z1)) → c20(U31'(tt, z0))
NATSFROM(z0) → c21
NATSFROM(z0) → c22
SEL(z0, z1) → c23(U41'(tt, z0, z1))
SND(pair(z0, z1)) → c24(U51'(tt, z1))
SPLITAT(0, z0) → c25
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
TAIL(cons(z0, z1)) → c27(U71'(tt, activate(z1)), ACTIVATE(z1))
TAKE(z0, z1) → c28(U81'(tt, z0, z1))
ACTIVATE(n__natsFrom(z0)) → c29(NATSFROM(z0))
ACTIVATE(z0) → c30
S tuples:
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U21'(tt, z0) → c2(U22'(tt, activate(z0)), ACTIVATE(z0))
U22'(tt, z0) → c3(ACTIVATE(z0))
U31'(tt, z0) → c4(U32'(tt, activate(z0)), ACTIVATE(z0))
U32'(tt, z0) → c5(ACTIVATE(z0))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U51'(tt, z0) → c8(U52'(tt, activate(z0)), ACTIVATE(z0))
U52'(tt, z0) → c9(ACTIVATE(z0))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1))
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2))
U71'(tt, z0) → c14(U72'(tt, activate(z0)), ACTIVATE(z0))
U72'(tt, z0) → c15(ACTIVATE(z0))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
FST(pair(z0, z1)) → c19(U21'(tt, z0))
HEAD(cons(z0, z1)) → c20(U31'(tt, z0))
NATSFROM(z0) → c21
NATSFROM(z0) → c22
SEL(z0, z1) → c23(U41'(tt, z0, z1))
SND(pair(z0, z1)) → c24(U51'(tt, z1))
SPLITAT(0, z0) → c25
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
TAIL(cons(z0, z1)) → c27(U71'(tt, activate(z1)), ACTIVATE(z1))
TAKE(z0, z1) → c28(U81'(tt, z0, z1))
ACTIVATE(n__natsFrom(z0)) → c29(NATSFROM(z0))
ACTIVATE(z0) → c30
K tuples:none
Defined Rule Symbols:
U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate
Defined Pair Symbols:
U11', U12', U21', U22', U31', U32', U41', U42', U51', U52', U61', U62', U63', U64', U71', U72', U81', U82', AFTERNTH, FST, HEAD, NATSFROM, SEL, SND, SPLITAT, TAIL, TAKE, ACTIVATE
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30
(3) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)
Removed 2 leading nodes:
SEL(z0, z1) → c23(U41'(tt, z0, z1))
TAKE(z0, z1) → c28(U81'(tt, z0, z1))
Removed 18 trailing nodes:
U52'(tt, z0) → c9(ACTIVATE(z0))
U32'(tt, z0) → c5(ACTIVATE(z0))
U31'(tt, z0) → c4(U32'(tt, activate(z0)), ACTIVATE(z0))
HEAD(cons(z0, z1)) → c20(U31'(tt, z0))
U71'(tt, z0) → c14(U72'(tt, activate(z0)), ACTIVATE(z0))
U51'(tt, z0) → c8(U52'(tt, activate(z0)), ACTIVATE(z0))
NATSFROM(z0) → c22
TAIL(cons(z0, z1)) → c27(U71'(tt, activate(z1)), ACTIVATE(z1))
ACTIVATE(n__natsFrom(z0)) → c29(NATSFROM(z0))
FST(pair(z0, z1)) → c19(U21'(tt, z0))
SND(pair(z0, z1)) → c24(U51'(tt, z1))
U64'(pair(z0, z1), z2) → c13(ACTIVATE(z2))
U21'(tt, z0) → c2(U22'(tt, activate(z0)), ACTIVATE(z0))
NATSFROM(z0) → c21
SPLITAT(0, z0) → c25
U72'(tt, z0) → c15(ACTIVATE(z0))
U22'(tt, z0) → c3(ACTIVATE(z0))
ACTIVATE(z0) → c30
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1))
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1)))
U21(tt, z0) → U22(tt, activate(z0))
U22(tt, z0) → activate(z0)
U31(tt, z0) → U32(tt, activate(z0))
U32(tt, z0) → activate(z0)
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1))
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1)))
U51(tt, z0) → U52(tt, activate(z0))
U52(tt, z0) → activate(z0)
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2))
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2))
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1))
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1)
U71(tt, z0) → U72(tt, activate(z0))
U72(tt, z0) → activate(z0)
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1))
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1)))
afterNth(z0, z1) → U11(tt, z0, z1)
fst(pair(z0, z1)) → U21(tt, z0)
head(cons(z0, z1)) → U31(tt, z0)
natsFrom(z0) → cons(z0, n__natsFrom(s(z0)))
natsFrom(z0) → n__natsFrom(z0)
sel(z0, z1) → U41(tt, z0, z1)
snd(pair(z0, z1)) → U51(tt, z1)
splitAt(0, z0) → pair(nil, z0)
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2))
tail(cons(z0, z1)) → U71(tt, activate(z1))
take(z0, z1) → U81(tt, z0, z1)
activate(n__natsFrom(z0)) → natsFrom(z0)
activate(z0) → z0
Tuples:
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
S tuples:
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U12'(tt, z0, z1) → c1(SND(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U42'(tt, z0, z1) → c7(HEAD(afterNth(activate(z0), activate(z1))), AFTERNTH(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)), ACTIVATE(z0), ACTIVATE(z1), ACTIVATE(z2))
U63'(tt, z0, z1, z2) → c12(U64'(splitAt(activate(z0), activate(z2)), activate(z1)), SPLITAT(activate(z0), activate(z2)), ACTIVATE(z0), ACTIVATE(z2), ACTIVATE(z1))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
U82'(tt, z0, z1) → c17(FST(splitAt(activate(z0), activate(z1))), SPLITAT(activate(z0), activate(z1)), ACTIVATE(z0), ACTIVATE(z1))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)), ACTIVATE(z2))
K tuples:none
Defined Rule Symbols:
U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate
Defined Pair Symbols:
U11', U12', U41', U42', U61', U62', U63', U81', U82', AFTERNTH, SPLITAT
Compound Symbols:
c, c1, c6, c7, c10, c11, c12, c16, c17, c18, c26
(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 26 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1))
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1)))
U21(tt, z0) → U22(tt, activate(z0))
U22(tt, z0) → activate(z0)
U31(tt, z0) → U32(tt, activate(z0))
U32(tt, z0) → activate(z0)
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1))
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1)))
U51(tt, z0) → U52(tt, activate(z0))
U52(tt, z0) → activate(z0)
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2))
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2))
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1))
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1)
U71(tt, z0) → U72(tt, activate(z0))
U72(tt, z0) → activate(z0)
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1))
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1)))
afterNth(z0, z1) → U11(tt, z0, z1)
fst(pair(z0, z1)) → U21(tt, z0)
head(cons(z0, z1)) → U31(tt, z0)
natsFrom(z0) → cons(z0, n__natsFrom(s(z0)))
natsFrom(z0) → n__natsFrom(z0)
sel(z0, z1) → U41(tt, z0, z1)
snd(pair(z0, z1)) → U51(tt, z1)
splitAt(0, z0) → pair(nil, z0)
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2))
tail(cons(z0, z1)) → U71(tt, activate(z1))
take(z0, z1) → U81(tt, z0, z1)
activate(n__natsFrom(z0)) → natsFrom(z0)
activate(z0) → z0
Tuples:
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
S tuples:
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
K tuples:none
Defined Rule Symbols:
U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate
Defined Pair Symbols:
AFTERNTH, U11', U12', U41', U42', U61', U62', U63', U81', U82', SPLITAT
Compound Symbols:
c18, c, c1, c6, c7, c10, c11, c12, c16, c17, c26
(7) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)
The following tuples could be moved from S to K by knowledge propagation:
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1))
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1)))
U21(tt, z0) → U22(tt, activate(z0))
U22(tt, z0) → activate(z0)
U31(tt, z0) → U32(tt, activate(z0))
U32(tt, z0) → activate(z0)
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1))
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1)))
U51(tt, z0) → U52(tt, activate(z0))
U52(tt, z0) → activate(z0)
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2))
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2))
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1))
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1)
U71(tt, z0) → U72(tt, activate(z0))
U72(tt, z0) → activate(z0)
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1))
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1)))
afterNth(z0, z1) → U11(tt, z0, z1)
fst(pair(z0, z1)) → U21(tt, z0)
head(cons(z0, z1)) → U31(tt, z0)
natsFrom(z0) → cons(z0, n__natsFrom(s(z0)))
natsFrom(z0) → n__natsFrom(z0)
sel(z0, z1) → U41(tt, z0, z1)
snd(pair(z0, z1)) → U51(tt, z1)
splitAt(0, z0) → pair(nil, z0)
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2))
tail(cons(z0, z1)) → U71(tt, activate(z1))
take(z0, z1) → U81(tt, z0, z1)
activate(n__natsFrom(z0)) → natsFrom(z0)
activate(z0) → z0
Tuples:
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
S tuples:
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
K tuples:
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
Defined Rule Symbols:
U11, U12, U21, U22, U31, U32, U41, U42, U51, U52, U61, U62, U63, U64, U71, U72, U81, U82, afterNth, fst, head, natsFrom, sel, snd, splitAt, tail, take, activate
Defined Pair Symbols:
AFTERNTH, U11', U12', U41', U42', U61', U62', U63', U81', U82', SPLITAT
Compound Symbols:
c18, c, c1, c6, c7, c10, c11, c12, c16, c17, c26
(9) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
U11(tt, z0, z1) → U12(tt, activate(z0), activate(z1))
U12(tt, z0, z1) → snd(splitAt(activate(z0), activate(z1)))
U21(tt, z0) → U22(tt, activate(z0))
U22(tt, z0) → activate(z0)
U31(tt, z0) → U32(tt, activate(z0))
U32(tt, z0) → activate(z0)
U41(tt, z0, z1) → U42(tt, activate(z0), activate(z1))
U42(tt, z0, z1) → head(afterNth(activate(z0), activate(z1)))
U51(tt, z0) → U52(tt, activate(z0))
U52(tt, z0) → activate(z0)
U61(tt, z0, z1, z2) → U62(tt, activate(z0), activate(z1), activate(z2))
U62(tt, z0, z1, z2) → U63(tt, activate(z0), activate(z1), activate(z2))
U63(tt, z0, z1, z2) → U64(splitAt(activate(z0), activate(z2)), activate(z1))
U64(pair(z0, z1), z2) → pair(cons(activate(z2), z0), z1)
U71(tt, z0) → U72(tt, activate(z0))
U72(tt, z0) → activate(z0)
U81(tt, z0, z1) → U82(tt, activate(z0), activate(z1))
U82(tt, z0, z1) → fst(splitAt(activate(z0), activate(z1)))
afterNth(z0, z1) → U11(tt, z0, z1)
fst(pair(z0, z1)) → U21(tt, z0)
head(cons(z0, z1)) → U31(tt, z0)
sel(z0, z1) → U41(tt, z0, z1)
snd(pair(z0, z1)) → U51(tt, z1)
splitAt(0, z0) → pair(nil, z0)
splitAt(s(z0), cons(z1, z2)) → U61(tt, z0, z1, activate(z2))
tail(cons(z0, z1)) → U71(tt, activate(z1))
take(z0, z1) → U81(tt, z0, z1)
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
activate(n__natsFrom(z0)) → natsFrom(z0)
activate(z0) → z0
natsFrom(z0) → cons(z0, n__natsFrom(s(z0)))
natsFrom(z0) → n__natsFrom(z0)
Tuples:
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
S tuples:
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
K tuples:
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
Defined Rule Symbols:
activate, natsFrom
Defined Pair Symbols:
AFTERNTH, U11', U12', U41', U42', U61', U62', U63', U81', U82', SPLITAT
Compound Symbols:
c18, c, c1, c6, c7, c10, c11, c12, c16, c17, c26
(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
We considered the (Usable) Rules:
natsFrom(z0) → cons(z0, n__natsFrom(s(z0)))
activate(n__natsFrom(z0)) → natsFrom(z0)
activate(z0) → z0
natsFrom(z0) → n__natsFrom(z0)
And the Tuples:
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(AFTERNTH(x1, x2)) = [1] + x1 + x2
POL(SPLITAT(x1, x2)) = x1
POL(U11'(x1, x2, x3)) = x1 + x2 + x3
POL(U12'(x1, x2, x3)) = x2 + x3
POL(U41'(x1, x2, x3)) = [1] + x1 + x2 + x3
POL(U42'(x1, x2, x3)) = [1] + x1 + x2 + x3
POL(U61'(x1, x2, x3, x4)) = x2
POL(U62'(x1, x2, x3, x4)) = x2
POL(U63'(x1, x2, x3, x4)) = x2
POL(U81'(x1, x2, x3)) = x2 + x3
POL(U82'(x1, x2, x3)) = x2
POL(activate(x1)) = x1
POL(c(x1)) = x1
POL(c1(x1)) = x1
POL(c10(x1)) = x1
POL(c11(x1)) = x1
POL(c12(x1)) = x1
POL(c16(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c26(x1)) = x1
POL(c6(x1)) = x1
POL(c7(x1)) = x1
POL(cons(x1, x2)) = [1]
POL(n__natsFrom(x1)) = [1]
POL(natsFrom(x1)) = [1]
POL(s(x1)) = [1] + x1
POL(tt) = [1]
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
activate(n__natsFrom(z0)) → natsFrom(z0)
activate(z0) → z0
natsFrom(z0) → cons(z0, n__natsFrom(s(z0)))
natsFrom(z0) → n__natsFrom(z0)
Tuples:
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
S tuples:
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
K tuples:
U41'(tt, z0, z1) → c6(U42'(tt, activate(z0), activate(z1)))
U42'(tt, z0, z1) → c7(AFTERNTH(activate(z0), activate(z1)))
U81'(tt, z0, z1) → c16(U82'(tt, activate(z0), activate(z1)))
U82'(tt, z0, z1) → c17(SPLITAT(activate(z0), activate(z1)))
AFTERNTH(z0, z1) → c18(U11'(tt, z0, z1))
U11'(tt, z0, z1) → c(U12'(tt, activate(z0), activate(z1)))
U12'(tt, z0, z1) → c1(SPLITAT(activate(z0), activate(z1)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
Defined Rule Symbols:
activate, natsFrom
Defined Pair Symbols:
AFTERNTH, U11', U12', U41', U42', U61', U62', U63', U81', U82', SPLITAT
Compound Symbols:
c18, c, c1, c6, c7, c10, c11, c12, c16, c17, c26
(13) CdtKnowledgeProof (EQUIVALENT transformation)
The following tuples could be moved from S to K by knowledge propagation:
U61'(tt, z0, z1, z2) → c10(U62'(tt, activate(z0), activate(z1), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
U62'(tt, z0, z1, z2) → c11(U63'(tt, activate(z0), activate(z1), activate(z2)))
U63'(tt, z0, z1, z2) → c12(SPLITAT(activate(z0), activate(z2)))
SPLITAT(s(z0), cons(z1, z2)) → c26(U61'(tt, z0, z1, activate(z2)))
Now S is empty
(14) BOUNDS(1, 1)